Search Results

Documents authored by Sozeau, Matthieu

Document
DOI: 10.4230/LIPIcs.FSCD.2018.29
Cumulative Inductive Types In Coq

Authors: Amin Timany and Matthieu Sozeau

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
In order to avoid well-known paradoxes associated with self-referential definitions, higher-order dependent type theories stratify the theory using a countably infinite hierarchy of universes (also known as sorts), Type_0 : Type_1 : *s. Such type systems are called cumulative if for any type A we have that A : Type_i implies A : Type_{i+1}. The Predicative Calculus of Inductive Constructions (pCIC) which forms the basis of the Coq proof assistant, is one such system. In this paper we present the Predicative Calculus of Cumulative Inductive Constructions (pCuIC) which extends the cumulativity relation to inductive types. We discuss cumulative inductive types as present in Coq 8.7 and their application to formalization and definitional translations.
Cite as

Amin Timany and Matthieu Sozeau. Cumulative Inductive Types In Coq. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{timany_et_al:LIPIcs.FSCD.2018.29,
  author =	{Timany, Amin and Sozeau, Matthieu},
  title =	{{Cumulative Inductive Types In Coq}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{29:1--29:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.29},
  URN =		{urn:nbn:de:0030-drops-91991},
  doi =		{10.4230/LIPIcs.FSCD.2018.29},
  annote =	{Keywords: Coq, Proof Assistants, Inductive Types, Universes, Cumulativity}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2014
LIPIcs, Volume 39, TYPES'14, Complete Volume

Authors: Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract
LIPIcs, Volume 39, TYPES'14, Complete Volume
Cite as

20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Proceedings{herbelin_et_al:LIPIcs.TYPES.2014,
  title =	{{LIPIcs, Volume 39, TYPES'14, Complete Volume}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014},
  URN =		{urn:nbn:de:0030-drops-55047},
  doi =		{10.4230/LIPIcs.TYPES.2014},
  annote =	{Keywords: Applicative (Functional) Programming, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Mathematical Logic}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2014.i
Front Matter, Table of Contents, Preface, Authors Index

Authors: Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract
Front Matter, Table of Contents, Preface, Authors Index
Cite as

20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. i-x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{herbelin_et_al:LIPIcs.TYPES.2014.i,
  author =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  title =	{{Front Matter, Table of Contents, Preface, Authors Index}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{i--x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.i},
  URN =		{urn:nbn:de:0030-drops-54888},
  doi =		{10.4230/LIPIcs.TYPES.2014.i},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Authors Index}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact